Field of the Invention
The invention relates to a method and a configuration for comparison of a first characteristic with predetermined characteristics of a technical system.
Model checking (MC) is a technique for verifying characteristics of a technical system using specific methods. In the past, a major complexity problem (state explosion problem) has occasionally arisen when this procedure was applied to the technical system. As a result of this, considerable efforts are being made to separate out a portion of a system that is to be verified, which is relevant for analysis and can be verified practically. Even then, the verification process often fails due to existing resource limits (computation performance, memory space).
As described by Kxc3xchlmann and Krohm, in xe2x80x9cEquivalence Checking Using Cuts and Heapsxe2x80x9d, 34th ACM/IEEE Design Automation Conference, 1997, pp.263-68, listed at [1] below, two circuits can be compared by means of binary decision diagrams (BDDs). In particular, this is aimed at highly complex digital circuits which are intended to be compared with one another, and for which structural similarities are determined (combinatorial circuit verification).
A first approach for combinatorial circuit verification attempts to produce functional implications by generating test patterns which are applied to the circuits to be compared (ATPG method). In this case, the object is to prove that an exclusive-or function between two output values to be compared cannot result in a logic xe2x80x9c1xe2x80x9d.
Another approach for combinatorial circuit verification is based on a canonic description of Boolean functions. Such a canonic description is represented by BDDs or specific variants of BDDs, for example by Reduced Ordered BDDs (ROBDDs). In this context, see [2] Jain, et al., xe2x80x9cA Survey of Techniques for Formal Verification of Combinatorial Circuitsxe2x80x9d, Proc. Int. Conf. on Computer Design (ICCD), 1997, pp.445-54, listed at [2] below. One special problem of BDDs is that of their exponentially rising memory space requirement.
What is referred to as an SAT comparison method (also SAT comparator; SAT=xe2x80x9cSatisfiabilityxe2x80x9d) is known from J. P. M. Silva: xe2x80x9cAn Overview of Backtrack Search Satisfiability Algorithms,xe2x80x9d, 5th Int. Symposium on Artificial Intelligence and Mathematics, 1998, listed at [3] below; Bayardo, Jr. and Schrag, xe2x80x9cUsing CSP Look-Back Techniques to Solve Real-World SAT-Instancesxe2x80x9d, Proc. of the National Conf. on Artificial Intelligence, pp.203-08, July 1997, listed at [4] below; and Davis and Putnam: xe2x80x9cA Computing Procedure for Quantification Theoryxe2x80x9d, Journal of the Association for Computing Machinery, Vol. 7, Number 3, July 1960, pp.125-39, listed at [7] below. The SAT comparison method is distinguished by searching systematically for solutions for any given Boolean notations in the form
(k1k2) (k3{overscore (k5)}) (k2{overscore (k4)})xe2x80x83xe2x80x83(1)
If the entire search area is exhausted without any solution being found during the search, then the fundamental Boolean problem cannot be solved.
The object of the present invention is to provide a method and a device for comparing a first characteristic with a predetermined characteristics of a technical system which overcomes the above-noted deficiencies and disadvantages of the prior art devices and methods of this general kind, and which ensures automatic solution of the comparison problem.
With the above and other objects in view there is provided, in accordance with the invention, a method of comparing a first characteristic with predetermined characteristics of a technical system, which comprises:
defining at least two comparison methods, each capable of carrying out a comparison of a Boolean function of the first characteristic with Boolean functions of the predetermined characteristics of the technical system; and
processing the at least two comparison methods in a predetermined sequence until a result of the comparison is defined.
In order to achieve the object, a method is specified for comparison of a first characteristic with predetermined characteristics of a technical system, in which at least two comparison methods are provided, each of which can carry out a comparison of the first characteristic with the predetermined characteristics of the technical system. The at least two comparison methods are processed in a predetermined sequence until a result of the comparison is defined.
In this case, it is particularly advantageous for different comparison methods to be processed automatically.
One development is for the result of the comparison to be equality of or a difference between the first characteristic and the characteristics of the technical system.
In particular, the comparison process can be terminated as soon as a single difference is discovered.
Another development provides for the first characteristic to be verified by the technical system on the basis of equality.
The at least two comparison methods may, in particular, be two of the following comparison methods:
a) SAT comparison method;
b) simulation method;
c) BDD method;
d) ATPG method;
e) methods based on internal equivalence points.
In particular, the BDD method may be an ROBDD method. Furthermore, the ROBDD method may be carried out with respect to its leaves or with respect to the sectional planes.
The technical system may be a circuit, in particular a digital electrical circuit.
In accordance with an added feature of the invention, at least a portion of the comparison is carried out with an intermediate result reducing the complexity of the overall comparison process. Reducing the complexity in this way allows a result to be achieved by means of a comparison method which originally failed in the overall comparison process.
In accordance with an additional feature of the invention, the intermediate result of a comparison method which was not carried out to the end, is used in a further comparison method (utilization of side effects). For example, a terminated BDD comparison method offers an approach for representing the problem to be solved (in this case, the overall comparison). This is done using a different comparison method as the intermediate result, which results in computation time and/or memory space being saved.
If a comparison results in inequality, then diagnosis information is preferably represented, allowing a user to determine the cause of the inequality.
In the course of one development, the technical system is described as a finite automatically controlled device. Furthermore, the first characteristic may be represented as a Boolean function. In addition, the first characteristic can describe a behavior of the technical system over a predetermined time interval.
Digital circuits are becoming increasingly larger. Any test for correct behavior is thus becoming more complex, more time-consuming, and more expensive. MC for circuits of an actual size is thus a critical economic factor. The convenience of the technique for the user is considerably simplified by the method described above and the associated configuration. The approach described here is not limited to hardware design, but can also be used for verification of software, whose behavior can preferably be described by a finite automatically controlled device (for example SDL programs, protocols).
In the present approach, a hybrid verification process, that is to say a process using a number of comparison methods, can be used to solve a verification task. A hybrid verification process is a framework which contains a set of partial verification processes (individual comparison methods). The hybrid verification process coordinates the way in which the partial verification processes operate. The aim is to use different verification processes to solve verification tasks which no verification process would have solved on its own. If none of the partial verification processes can solve a given verification task, then this verification task is broken down. To do this, subtasks are transferred to each partial verification process, which the latter can process subject to allocation of resources. If a threshold value for the allocation of associated resources is exceeded, the verification process terminates its processing. The hybrid verification process then decides whether the subtask will be handled by another partial verification process, whether the resources should be increased or whether to continue with a different subtask.
In the course of an additional refinement, a threshold value for resources to be provided (for example memory space or computation power) and/or time to be provided for carrying out the comparison method are/is defined for each comparison method, with the respective comparison method being ended as being unsuccessful if the threshold value is succeeded.
This is particularly advantageous when a single comparison method blocks a computer on which it is running, or no solution is defined in a predetermined time interval, for example due to rapidly rising complexity. In a case such as this, it is often better to work out a solution using the next comparison method.
Another development is for the sequence of the comparison methods to be carried out to be adapted dynamically. This is preferably done by also recording which comparison method has defined the most results, with this xe2x80x9cbestxe2x80x9d comparison method being used first of all for future comparisons. The sequence is accordingly sorted with the xe2x80x9csecond-bestxe2x80x9d, the xe2x80x9cthird-bestxe2x80x9d etc. comparison methods.
The result of the comparison can be used to design, to adapt or to control the technical system.
Particular in the case of the circuit simulation, the result of the described comparison can be implemented directly, if it is positive, by a predetermined description form initiating a production process for the circuit.
With the above and other objects in view there is also provided, in accordance with the invention, a configuration for comparing a first characteristic with predetermined characteristics of a technical system, comprising a processor unit configured with at least two comparison methods, each comparison method allowing a Boolean function of the first characteristic to be compared with Boolean functions of the predetermined characteristics of the technical system; and
to process the at least two comparison methods in a predetermined sequence until a result of the comparison can be defined.
In other words, the processor unit is set up in such a manner that
a) at least two comparison methods are provided, each of which allows the first characteristic to be compared with the predetermined characteristics of the technical system;
b) the at least two comparison methods are processed in a predetermined sequence until a result of the comparison can be defined.
The configuration according to the invention is particularly suitable for carrying out the above-outlined method, or one of its developments.
Other features which are considered as characteristic for the invention are set forth in the appended claims.
Although the invention is illustrated and described herein as embodied in a method and configuration for comparison of a first characteristic with predetermined characteristics of a technical system, it is nevertheless not intended to be limited to the details shown, since various modifications and structural changes may be made therein without departing from the spirit of the invention and within the scope and range of equivalents of the claims.
The construction and method of operation of the invention, however, together with additional objects and advantages thereof will be best understood from the following description of specific embodiments when read in connection with the accompanying drawings.